0 Prolog
↳1 PrologToPiTRSProof (⇒, 0 ms)
↳2 PiTRS
↳3 DependencyPairsProof (⇔, 4 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 PiDP
↳7 PiDPToQDPProof (⇔, 21 ms)
↳8 QDP
↳9 QDPOrderProof (⇔, 150 ms)
↳10 QDP
↳11 DependencyGraphProof (⇔, 0 ms)
↳12 QDP
↳13 UsableRulesProof (⇔, 0 ms)
↳14 QDP
↳15 QReductionProof (⇔, 0 ms)
↳16 QDP
↳17 UsableRulesReductionPairsProof (⇔, 13 ms)
↳18 QDP
↳19 PisEmptyProof (⇔, 0 ms)
↳20 YES
p_in_g(cons(X, nil)) → p_out_g(cons(X, nil))
p_in_g(cons(s(s(X)), cons(Y, Xs))) → U1_g(X, Y, Xs, p_in_g(cons(X, cons(Y, Xs))))
p_in_g(cons(0, Xs)) → U3_g(Xs, p_in_g(Xs))
U3_g(Xs, p_out_g(Xs)) → p_out_g(cons(0, Xs))
U1_g(X, Y, Xs, p_out_g(cons(X, cons(Y, Xs)))) → U2_g(X, Y, Xs, p_in_g(cons(s(s(s(s(Y)))), Xs)))
U2_g(X, Y, Xs, p_out_g(cons(s(s(s(s(Y)))), Xs))) → p_out_g(cons(s(s(X)), cons(Y, Xs)))
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
p_in_g(cons(X, nil)) → p_out_g(cons(X, nil))
p_in_g(cons(s(s(X)), cons(Y, Xs))) → U1_g(X, Y, Xs, p_in_g(cons(X, cons(Y, Xs))))
p_in_g(cons(0, Xs)) → U3_g(Xs, p_in_g(Xs))
U3_g(Xs, p_out_g(Xs)) → p_out_g(cons(0, Xs))
U1_g(X, Y, Xs, p_out_g(cons(X, cons(Y, Xs)))) → U2_g(X, Y, Xs, p_in_g(cons(s(s(s(s(Y)))), Xs)))
U2_g(X, Y, Xs, p_out_g(cons(s(s(s(s(Y)))), Xs))) → p_out_g(cons(s(s(X)), cons(Y, Xs)))
P_IN_G(cons(s(s(X)), cons(Y, Xs))) → U1_G(X, Y, Xs, p_in_g(cons(X, cons(Y, Xs))))
P_IN_G(cons(s(s(X)), cons(Y, Xs))) → P_IN_G(cons(X, cons(Y, Xs)))
P_IN_G(cons(0, Xs)) → U3_G(Xs, p_in_g(Xs))
P_IN_G(cons(0, Xs)) → P_IN_G(Xs)
U1_G(X, Y, Xs, p_out_g(cons(X, cons(Y, Xs)))) → U2_G(X, Y, Xs, p_in_g(cons(s(s(s(s(Y)))), Xs)))
U1_G(X, Y, Xs, p_out_g(cons(X, cons(Y, Xs)))) → P_IN_G(cons(s(s(s(s(Y)))), Xs))
p_in_g(cons(X, nil)) → p_out_g(cons(X, nil))
p_in_g(cons(s(s(X)), cons(Y, Xs))) → U1_g(X, Y, Xs, p_in_g(cons(X, cons(Y, Xs))))
p_in_g(cons(0, Xs)) → U3_g(Xs, p_in_g(Xs))
U3_g(Xs, p_out_g(Xs)) → p_out_g(cons(0, Xs))
U1_g(X, Y, Xs, p_out_g(cons(X, cons(Y, Xs)))) → U2_g(X, Y, Xs, p_in_g(cons(s(s(s(s(Y)))), Xs)))
U2_g(X, Y, Xs, p_out_g(cons(s(s(s(s(Y)))), Xs))) → p_out_g(cons(s(s(X)), cons(Y, Xs)))
P_IN_G(cons(s(s(X)), cons(Y, Xs))) → U1_G(X, Y, Xs, p_in_g(cons(X, cons(Y, Xs))))
P_IN_G(cons(s(s(X)), cons(Y, Xs))) → P_IN_G(cons(X, cons(Y, Xs)))
P_IN_G(cons(0, Xs)) → U3_G(Xs, p_in_g(Xs))
P_IN_G(cons(0, Xs)) → P_IN_G(Xs)
U1_G(X, Y, Xs, p_out_g(cons(X, cons(Y, Xs)))) → U2_G(X, Y, Xs, p_in_g(cons(s(s(s(s(Y)))), Xs)))
U1_G(X, Y, Xs, p_out_g(cons(X, cons(Y, Xs)))) → P_IN_G(cons(s(s(s(s(Y)))), Xs))
p_in_g(cons(X, nil)) → p_out_g(cons(X, nil))
p_in_g(cons(s(s(X)), cons(Y, Xs))) → U1_g(X, Y, Xs, p_in_g(cons(X, cons(Y, Xs))))
p_in_g(cons(0, Xs)) → U3_g(Xs, p_in_g(Xs))
U3_g(Xs, p_out_g(Xs)) → p_out_g(cons(0, Xs))
U1_g(X, Y, Xs, p_out_g(cons(X, cons(Y, Xs)))) → U2_g(X, Y, Xs, p_in_g(cons(s(s(s(s(Y)))), Xs)))
U2_g(X, Y, Xs, p_out_g(cons(s(s(s(s(Y)))), Xs))) → p_out_g(cons(s(s(X)), cons(Y, Xs)))
U1_G(X, Y, Xs, p_out_g(cons(X, cons(Y, Xs)))) → P_IN_G(cons(s(s(s(s(Y)))), Xs))
P_IN_G(cons(s(s(X)), cons(Y, Xs))) → U1_G(X, Y, Xs, p_in_g(cons(X, cons(Y, Xs))))
P_IN_G(cons(s(s(X)), cons(Y, Xs))) → P_IN_G(cons(X, cons(Y, Xs)))
P_IN_G(cons(0, Xs)) → P_IN_G(Xs)
p_in_g(cons(X, nil)) → p_out_g(cons(X, nil))
p_in_g(cons(s(s(X)), cons(Y, Xs))) → U1_g(X, Y, Xs, p_in_g(cons(X, cons(Y, Xs))))
p_in_g(cons(0, Xs)) → U3_g(Xs, p_in_g(Xs))
U3_g(Xs, p_out_g(Xs)) → p_out_g(cons(0, Xs))
U1_g(X, Y, Xs, p_out_g(cons(X, cons(Y, Xs)))) → U2_g(X, Y, Xs, p_in_g(cons(s(s(s(s(Y)))), Xs)))
U2_g(X, Y, Xs, p_out_g(cons(s(s(s(s(Y)))), Xs))) → p_out_g(cons(s(s(X)), cons(Y, Xs)))
U1_G(X, Y, Xs, p_out_g(cons(X, cons(Y, Xs)))) → P_IN_G(cons(s(s(s(s(Y)))), Xs))
P_IN_G(cons(s(s(X)), cons(Y, Xs))) → U1_G(X, Y, Xs, p_in_g(cons(X, cons(Y, Xs))))
P_IN_G(cons(s(s(X)), cons(Y, Xs))) → P_IN_G(cons(X, cons(Y, Xs)))
P_IN_G(cons(0, Xs)) → P_IN_G(Xs)
p_in_g(cons(X, nil)) → p_out_g(cons(X, nil))
p_in_g(cons(s(s(X)), cons(Y, Xs))) → U1_g(X, Y, Xs, p_in_g(cons(X, cons(Y, Xs))))
p_in_g(cons(0, Xs)) → U3_g(Xs, p_in_g(Xs))
U3_g(Xs, p_out_g(Xs)) → p_out_g(cons(0, Xs))
U1_g(X, Y, Xs, p_out_g(cons(X, cons(Y, Xs)))) → U2_g(X, Y, Xs, p_in_g(cons(s(s(s(s(Y)))), Xs)))
U2_g(X, Y, Xs, p_out_g(cons(s(s(s(s(Y)))), Xs))) → p_out_g(cons(s(s(X)), cons(Y, Xs)))
p_in_g(x0)
U3_g(x0, x1)
U1_g(x0, x1, x2, x3)
U2_g(x0, x1, x2, x3)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
P_IN_G(cons(s(s(X)), cons(Y, Xs))) → U1_G(X, Y, Xs, p_in_g(cons(X, cons(Y, Xs))))
P_IN_G(cons(0, Xs)) → P_IN_G(Xs)
POL(0) = 1
POL(P_IN_G(x1)) = x1
POL(U1_G(x1, x2, x3, x4)) = 1 + x2 + x3
POL(U1_g(x1, x2, x3, x4)) = 0
POL(U2_g(x1, x2, x3, x4)) = 0
POL(U3_g(x1, x2)) = 0
POL(cons(x1, x2)) = 1 + x1 + x2
POL(nil) = 1
POL(p_in_g(x1)) = x1
POL(p_out_g(x1)) = 1
POL(s(x1)) = x1
U1_G(X, Y, Xs, p_out_g(cons(X, cons(Y, Xs)))) → P_IN_G(cons(s(s(s(s(Y)))), Xs))
P_IN_G(cons(s(s(X)), cons(Y, Xs))) → P_IN_G(cons(X, cons(Y, Xs)))
p_in_g(cons(X, nil)) → p_out_g(cons(X, nil))
p_in_g(cons(s(s(X)), cons(Y, Xs))) → U1_g(X, Y, Xs, p_in_g(cons(X, cons(Y, Xs))))
p_in_g(cons(0, Xs)) → U3_g(Xs, p_in_g(Xs))
U3_g(Xs, p_out_g(Xs)) → p_out_g(cons(0, Xs))
U1_g(X, Y, Xs, p_out_g(cons(X, cons(Y, Xs)))) → U2_g(X, Y, Xs, p_in_g(cons(s(s(s(s(Y)))), Xs)))
U2_g(X, Y, Xs, p_out_g(cons(s(s(s(s(Y)))), Xs))) → p_out_g(cons(s(s(X)), cons(Y, Xs)))
p_in_g(x0)
U3_g(x0, x1)
U1_g(x0, x1, x2, x3)
U2_g(x0, x1, x2, x3)
P_IN_G(cons(s(s(X)), cons(Y, Xs))) → P_IN_G(cons(X, cons(Y, Xs)))
p_in_g(cons(X, nil)) → p_out_g(cons(X, nil))
p_in_g(cons(s(s(X)), cons(Y, Xs))) → U1_g(X, Y, Xs, p_in_g(cons(X, cons(Y, Xs))))
p_in_g(cons(0, Xs)) → U3_g(Xs, p_in_g(Xs))
U3_g(Xs, p_out_g(Xs)) → p_out_g(cons(0, Xs))
U1_g(X, Y, Xs, p_out_g(cons(X, cons(Y, Xs)))) → U2_g(X, Y, Xs, p_in_g(cons(s(s(s(s(Y)))), Xs)))
U2_g(X, Y, Xs, p_out_g(cons(s(s(s(s(Y)))), Xs))) → p_out_g(cons(s(s(X)), cons(Y, Xs)))
p_in_g(x0)
U3_g(x0, x1)
U1_g(x0, x1, x2, x3)
U2_g(x0, x1, x2, x3)
P_IN_G(cons(s(s(X)), cons(Y, Xs))) → P_IN_G(cons(X, cons(Y, Xs)))
p_in_g(x0)
U3_g(x0, x1)
U1_g(x0, x1, x2, x3)
U2_g(x0, x1, x2, x3)
p_in_g(x0)
U3_g(x0, x1)
U1_g(x0, x1, x2, x3)
U2_g(x0, x1, x2, x3)
P_IN_G(cons(s(s(X)), cons(Y, Xs))) → P_IN_G(cons(X, cons(Y, Xs)))
No rules are removed from R.
P_IN_G(cons(s(s(X)), cons(Y, Xs))) → P_IN_G(cons(X, cons(Y, Xs)))
POL(P_IN_G(x1)) = 2·x1
POL(cons(x1, x2)) = 2·x1 + x2
POL(s(x1)) = 2·x1